import Yices hiding (and, or, not, bits, le)
import qualified Yices as Y
import Data.List

type Binary = Nat -> Bool

bpp, steps, slots :: Nat
slots = 12 -- how many numbers
bpp   = 4  -- bits per pixel
steps = 1  -- how many transitions

decl :: (String -> a) -> String -> (a, a, a)
decl i n = (i n, i (n ++ "0"), i (n ++ "1"))

s' :: Ident (Nat -> Nat -> Bool)
((s',s),(s0',s0),(s1',s1)) = decl ident2 "s"

p', n' :: Ident Binary
((p',p),(p0',p0),(p1',p1)) = decl ident1 "p"
((n',n),(n0',n0),(n1',n1)) = decl ident1 "n"

-- Binary representation of a number
infix 4 .=
(.=) :: Term Binary -> Nat -> Prop
b .= n = conj $ zipWith beq (take width $ bits n) [b ! nat i | i <- [0..]]
  where
    bits = unfoldr (Just . \x -> (odd x, x `div` 2))
    beq True  = id
    beq False = non
    width = fromIntegral bpp

-- Successor arithmetic, tabular representation
follows :: Term Binary -> Term Binary -> Prop
x `follows` y = disj [ (x .= i+1) /\ (y .= i) | i <- [0..slots-1]] 

initial :: Prop
initial =
    idt p' .= 0 /\ idt n' .= 0
    /\ conj [Y.non (s i 3 /\ s i 2) | i <- [0..slots-1]]
    /\ conj [neqNum i j | i <- [0..slots-2], j <- [i+1, slots-1]]
  where
    neqNum i j = disj [xor' ! s i k ! s j k | k <- [0..bpp-1]]

final :: Prop
final = idt p' .= steps

trans :: Prop
trans = conj
    [ ifte (idt p0' .= 11)
        ((idt n1' `follows` idt n0') /\ (idt p1' .= 0))
        (idt p1' `follows` idt p0')
    , (idt p0' .= 0) ==> halfsort
    , conj [(idt p0' .= i) ==> stepsort i | i <- [1..slots-1]]
    ]
  where
    halfsort = conj [swap i (11-i) | i <- [0..(slots `div` 2)-1]]
    stepsort i = conj [step i j | j <- [0..slots-2]]
    step i j
        | j == i     = swap j (j+1)
        | j == i+1   = bool True -- NOP
        | otherwise = copy j j

copy :: Nat -> Nat -> Prop
copy i j = conj [iff' ! (s0 i k) ! (s1 j k) | k <- [0..bpp-1]]

swap :: Nat -> Nat -> Prop
swap i j = ifte (le i j)
    (copy i i /\ copy j j)
    (copy i j /\ copy j i)

le :: Nat -> Nat -> Prop
le i j = cmp (bpp - 1)
  where
    cmp 0 = Y.non (s0 i 0) /\ s0 j 0
    cmp k =
        ifte (Y.non (s0 i k) /\ s0 j k) -- s[i] < s[j]
            (bool True)
            (ifte (s0 i k /\ Y.non (s0 j k))
                (bool False)
                (cmp $ k-1))

main = printBddReach initial trans final
